00100	MATCHA(U,V,L) ← 
00200		IF L EQ 'NO THEN 'NO
00300		ELSE IF ATOM U THEN
00400			(IF ISVAR U THEN
00500				(LAMBDA (W);
00600					IF NULL W THEN (U.V).SUBST(V,U,L)
00700					ELSE IF CDR W = V THEN L
00800					ELSE 'NO)
00900				(ASSOC(U,L))
01000			 ELSE IF ATOM V THEN
01100				(IF ISVAR V THEN
01200					(LAMBDA (W);
01300						IF NULL W THEN
01400							(V.U).SUBST(U,V,L)
01500						ELSE IF CDR W = U THEN L
01600						ELSE 'NO)
01700				(ASSOC(V,L))
01800				 ELSE IF U = V THEN L
01900				 ELSE 'NO)
02000			 ELSE 'NO)
02100		ELSE IF ATOM V THEN
02200			(IF ISVAR V THEN
02300				(LAMBDA (W);
02400					IF NULL W THEN (V.U).SUBST(U,V,L)
02500					ELSE IF CDR W = U THEN L
02600					ELSE 'NO)
02700				(ASSOC(V,L))
02800			 ELSE 'NO)
02900		ELSE (LAMBDA(W);MATCHA(SUBLIS(W,CAR U),
03000			SUBLIS(W,CAR V),W))(MATCHA(CDR U,CDR V,L));
03100	
03200	ISVAR X ← X MEMBER '(X Y Z U V W);
03300	
03400	SUBLIS(W,E) ←
03500		IF ATOM E THEN
03600			(LAMBDA (Z); IF NULL Z THEN E ELSE CDR Z)
03700			(ASSOC(E,W))
03800		ELSE (LAMBDA(X,Y);
03900			IF X EQ CAR E AND Y EQ CDR E THEN E ELSE X.Y)
04000			(SUBLIS(W, CAR E),SUBLIS(W,CDR E));